Nuprl Lemma : es-send_wf
0,22
postcript
pdf
es
:ES,
i
:Id. Send(
i
)
k
:Knd
kindtype(
i
;
k
)
(
x
:Id
vartype(
i
;
x
))
(Msg List)
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
kindtype(
i
;
k
)
,
vartype(
i
;
x
)
,
Msg
,
Send(
i
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
if
b
t
else
f
fi
,
isrcv(
k
)
,
es-M(
es
)
,
lnk(
k
)
,
tag(
k
)
,
es-V(
es
)
,
act(
k
)
,
es-T(
es
)
,
es-Send(
es
)
,
1of(
t
)
,
2of(
t
)
,
x
.
t
(
x
)
,
x
,
y
.
t
(
x
;
y
)
,
isl(
x
)
,
outl(
x
)
,
outr(
x
)
,
true
,
false
,
islocal(
k
)
,
b
,
ES
,
Knd
,
P
&
Q
,
P
Q
,
x
(
s
)
,
x
(
s1
,
s2
)
Lemmas
subtype
rel
dep
function
,
Knd
wf
,
kindcase
wf
,
IdLnk
wf
,
Msg
wf
,
subtype
rel
self
,
Id
wf
,
event
system
wf
origin
es:ES, i:Id. Send(i) 
k:Knd
kindtype(i;k)(x:Idvartype(i;x))(Msg List) es:ES, i:Id. Send(i) k:Kndkindtype(i;k)(x:Idvartype(i;x))(Msg List) x:A. B(x) T
t else f fi
x. t(x)x,y. t(x;y)
b
Q